YES 31.299
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Lambda Reductions:
The following Lambda expression
\nd→n * radix + d
is transformed to
readInt0 | radix n d | = n * radix + d |
The following Lambda expression
\vu77→
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt1 | radix digToInt vu77 | =
case | vu77 of | | (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
|
The following Lambda expression
\d→fromEnum d - fromEnum_0
is transformed to
readOct0 | d | = fromEnum d - fromEnum_0 |
The following Lambda expression
\vu68→
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull0 | vu68 | =
case | vu68 of | | (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
|
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Case Reductions:
The following Case expression
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt10 | radix digToInt (ds,r) | = (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
readInt10 | radix digToInt _ | = [] |
The following Case expression
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull00 | (cs@(_ : _),t) | = (cs,t) : [] |
nonnull00 | _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)
is replaced by the following term
vy : vz
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (ww : wx) | |
is transformed to
span | p [] | = span3 p [] |
span | p (ww : wx) | = span2 p (ww : wx) |
span2 | p (ww : wx) | =
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | xx xy | = span2 xx xy |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Zs0 | xz yu (wz,zs) | = zs |
span2Span0 | xz yu p ww wx True | = ([],ww : wx) |
span2Ys | xz yu | = span2Ys0 xz yu (span2Vu43 xz yu) |
span2Vu43 | xz yu | = span xz yu |
span2Zs | xz yu | = span2Zs0 xz yu (span2Vu43 xz yu) |
span2Ys0 | xz yu (ys,wy) | = ys |
span2Span1 | xz yu p ww wx True | = (ww : span2Ys xz yu,span2Zs xz yu) |
span2Span1 | xz yu p ww wx False | = span2Span0 xz yu p ww wx otherwise |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
| ((readOct :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| (readOct :: [Char] -> [(Int,[Char])]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(yv70, yv71), yv8) → new_psPs(yv71, yv8)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(yv70, yv71), yv8) → new_psPs(yv71, yv8)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs0(Char(Succ(yv8500)), yv86, yv87, yv88) → new_span2Zs00(yv8500, yv86, yv8500, yv87, yv88)
new_span2Zs00(yv107, yv108, Succ(yv1090), Zero, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
new_span2Zs01(yv128, yv129, Zero, Zero) → new_span2Zs03(yv128, yv129)
new_span2Zs(:(yv660, yv661)) → new_span2Zs0(yv660, yv661, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs02(yv107, yv108, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
new_span2Zs01(yv128, yv129, Succ(yv1300), Succ(yv1310)) → new_span2Zs01(yv128, yv129, yv1300, yv1310)
new_span2Zs00(yv107, yv108, Zero, Zero, yv111) → new_span2Zs02(yv107, yv108, yv111)
new_span2Zs01(yv128, yv129, Zero, Succ(yv1310)) → new_span2Zs(yv129)
new_span2Zs00(yv107, yv108, Succ(yv1090), Succ(yv1100), yv111) → new_span2Zs00(yv107, yv108, yv1090, yv1100, yv111)
new_span2Zs03(yv128, yv129) → new_span2Zs(yv129)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs01(yv128, yv129, Succ(yv1300), Succ(yv1310)) → new_span2Zs01(yv128, yv129, yv1300, yv1310)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
- new_span2Zs00(yv107, yv108, Succ(yv1090), Succ(yv1100), yv111) → new_span2Zs00(yv107, yv108, yv1090, yv1100, yv111)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
- new_span2Zs0(Char(Succ(yv8500)), yv86, yv87, yv88) → new_span2Zs00(yv8500, yv86, yv8500, yv87, yv88)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 3 >= 4, 4 >= 5
- new_span2Zs(:(yv660, yv661)) → new_span2Zs0(yv660, yv661, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
- new_span2Zs03(yv128, yv129) → new_span2Zs(yv129)
The graph contains the following edges 2 >= 1
- new_span2Zs01(yv128, yv129, Zero, Succ(yv1310)) → new_span2Zs(yv129)
The graph contains the following edges 2 >= 1
- new_span2Zs00(yv107, yv108, Succ(yv1090), Zero, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
The graph contains the following edges 1 >= 1, 2 >= 2
- new_span2Zs00(yv107, yv108, Zero, Zero, yv111) → new_span2Zs02(yv107, yv108, yv111)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
- new_span2Zs01(yv128, yv129, Zero, Zero) → new_span2Zs03(yv128, yv129)
The graph contains the following edges 1 >= 1, 2 >= 2
- new_span2Zs02(yv107, yv108, yv111) → new_span2Zs01(yv107, yv108, Succ(yv107), Succ(yv111))
The graph contains the following edges 1 >= 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNat(Succ(yv1040), Succ(yv1050)) → new_primMinusNat(yv1040, yv1050)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNat(Succ(yv1040), Succ(yv1050)) → new_primMinusNat(yv1040, yv1050)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yv2130), Succ(yv19700)) → new_primPlusNat(yv2130, yv19700)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yv2130), Succ(yv19700)) → new_primPlusNat(yv2130, yv19700)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yv19100), yv190) → new_primMulNat(yv19100, yv190)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yv19100), yv190) → new_primMulNat(yv19100, yv190)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Zero, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
new_foldl2(yv190, yv191, yv192, yv193, yv196, bb) → new_foldl4(yv190, yv191, new_pt(yv192, bb), yv193, bb)
new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Succ(yv1650), yv166, ba) → new_foldl(yv160, yv161, yv162, yv163, yv1640, yv1650, yv166, ba)
new_foldl(yv160, yv161, yv162, yv163, Zero, Zero, yv166, ba) → new_foldl1(yv160, yv161, yv162, yv163, yv166, ba)
new_foldl6(yv147, yv154, Char(Succ(yv15000)), yv151, yv152, yv153, bd) → new_foldl(yv147, yv154, yv15000, yv151, yv15000, yv152, yv153, bd)
new_foldl1(yv160, yv161, yv162, yv163, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
new_foldl3(yv190, yv191, yv192, yv193, bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
new_foldl5(yv206, yv207, yv208, yv209, yv210, yv211, yv212, bc) → new_foldl6(yv206, new_readInt0(yv206, yv207, yv208, bc), yv209, yv210, yv211, yv212, bc)
new_foldl0(yv190, yv191, yv192, yv193, Zero, Succ(yv1950), bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
new_foldl0(yv190, yv191, yv192, yv193, Succ(yv1940), Succ(yv1950), bb) → new_foldl0(yv190, yv191, yv192, yv193, yv1940, yv1950, bb)
new_foldl4(yv190, yv191, yv197, :(yv1930, yv1931), bb) → new_foldl5(yv190, yv191, yv197, yv1930, yv1931, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
new_foldl0(yv190, yv191, yv192, yv193, Zero, Zero, bb) → new_foldl3(yv190, yv191, yv192, yv193, bb)
The TRS R consists of the following rules:
new_span2Zs1(:(yv660, yv661)) → new_span2Zs05(yv660, yv661, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs09(yv128, yv129) → new_span2Zs04(yv128, yv129, new_span2Zs1(yv129))
new_readInt0(yv190, Neg(yv1910), Neg(yv1970), ty_Int) → Neg(new_primPlusNat0(new_primMulNat0(yv1910, yv190), yv1970))
new_span2Zs06(yv107, yv108, Succ(yv1090), Zero, yv111) → new_span2Zs010(yv107, yv108, yv111)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_pt(yv76, ty_Int) → new_primMinusInt(yv76, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs010(yv107, yv108, yv111) → new_span2Zs08(yv107, yv108, Succ(yv107), Succ(yv111))
new_primMulNat0(Succ(yv19100), yv190) → new_primPlusNat0(new_primMulNat0(yv19100, yv190), Succ(yv190))
new_primMulNat0(Zero, yv190) → Zero
new_span2Zs04(yv128, yv129, yv133) → yv133
new_primMinusNat0(Zero, Succ(yv1050)) → Neg(Succ(yv1050))
new_primPlusNat0(Succ(yv2130), Succ(yv19700)) → Succ(Succ(new_primPlusNat0(yv2130, yv19700)))
new_primMinusInt(yv104, yv105) → new_primMinusNat0(yv104, yv105)
new_span2Zs08(yv128, yv129, Succ(yv1300), Succ(yv1310)) → new_span2Zs08(yv128, yv129, yv1300, yv1310)
new_span2Zs06(yv107, yv108, Zero, Succ(yv1100), yv111) → new_span2Zs07(yv107, yv108)
new_readInt0(yv190, Pos(yv1910), Neg(yv1970), ty_Int) → new_primMinusNat0(new_primMulNat0(yv1910, yv190), yv1970)
new_readInt0(yv190, Neg(yv1910), Pos(yv1970), ty_Int) → new_primMinusNat0(yv1970, new_primMulNat0(yv1910, yv190))
new_span2Zs07(yv107, yv108) → :(Char(Succ(yv107)), yv108)
new_primPlusNat0(Zero, Zero) → Zero
new_span2Zs1([]) → []
new_readInt0(yv190, Pos(yv1910), Pos(yv1970), ty_Int) → Pos(new_primPlusNat0(new_primMulNat0(yv1910, yv190), yv1970))
new_span2Zs06(yv107, yv108, Zero, Zero, yv111) → new_span2Zs010(yv107, yv108, yv111)
new_span2Zs08(yv128, yv129, Succ(yv1300), Zero) → new_span2Zs07(yv128, yv129)
new_span2Zs08(yv128, yv129, Zero, Zero) → new_span2Zs09(yv128, yv129)
new_pt(yv76, ty_Integer) → error([])
new_span2Zs06(yv107, yv108, Succ(yv1090), Succ(yv1100), yv111) → new_span2Zs06(yv107, yv108, yv1090, yv1100, yv111)
new_span2Zs05(Char(Succ(yv8500)), yv86, yv87, yv88) → new_span2Zs06(yv8500, yv86, yv8500, yv87, yv88)
new_readInt0(yv190, yv191, yv197, ty_Integer) → error([])
new_primMinusNat0(Succ(yv1040), Zero) → Pos(Succ(yv1040))
new_span2Zs08(yv128, yv129, Zero, Succ(yv1310)) → new_span2Zs09(yv128, yv129)
new_span2Zs05(Char(Zero), yv86, yv87, yv88) → :(Char(Zero), yv86)
new_primPlusNat0(Zero, Succ(yv19700)) → Succ(yv19700)
new_primPlusNat0(Succ(yv2130), Zero) → Succ(yv2130)
new_primMinusNat0(Succ(yv1040), Succ(yv1050)) → new_primMinusNat0(yv1040, yv1050)
The set Q consists of the following terms:
new_primMinusInt(x0, x1)
new_primMinusNat0(Succ(x0), Succ(x1))
new_span2Zs05(Char(Zero), x0, x1, x2)
new_span2Zs06(x0, x1, Zero, Succ(x2), x3)
new_readInt0(x0, Pos(x1), Pos(x2), ty_Int)
new_span2Zs04(x0, x1, x2)
new_pt(x0, ty_Int)
new_readInt0(x0, Neg(x1), Neg(x2), ty_Int)
new_primPlusNat0(Succ(x0), Zero)
new_span2Zs05(Char(Succ(x0)), x1, x2, x3)
new_pt(x0, ty_Integer)
new_span2Zs1(:(x0, x1))
new_span2Zs06(x0, x1, Succ(x2), Succ(x3), x4)
new_span2Zs08(x0, x1, Succ(x2), Succ(x3))
new_span2Zs07(x0, x1)
new_primMinusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_span2Zs1([])
new_primMinusNat0(Succ(x0), Zero)
new_span2Zs08(x0, x1, Succ(x2), Zero)
new_primMulNat0(Succ(x0), x1)
new_readInt0(x0, x1, x2, ty_Integer)
new_span2Zs06(x0, x1, Zero, Zero, x2)
new_span2Zs010(x0, x1, x2)
new_span2Zs08(x0, x1, Zero, Succ(x2))
new_span2Zs06(x0, x1, Succ(x2), Zero, x3)
new_primMulNat0(Zero, x0)
new_span2Zs08(x0, x1, Zero, Zero)
new_span2Zs09(x0, x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMinusNat0(Zero, Succ(x0))
new_readInt0(x0, Neg(x1), Pos(x2), ty_Int)
new_readInt0(x0, Pos(x1), Neg(x2), ty_Int)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl4(yv190, yv191, yv197, :(yv1930, yv1931), bb) → new_foldl5(yv190, yv191, yv197, yv1930, yv1931, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 4 > 5, 5 >= 8
- new_foldl0(yv190, yv191, yv192, yv193, Succ(yv1940), Succ(yv1950), bb) → new_foldl0(yv190, yv191, yv192, yv193, yv1940, yv1950, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 > 6, 7 >= 7
- new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Succ(yv1650), yv166, ba) → new_foldl(yv160, yv161, yv162, yv163, yv1640, yv1650, yv166, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 > 6, 7 >= 7, 8 >= 8
- new_foldl6(yv147, yv154, Char(Succ(yv15000)), yv151, yv152, yv153, bd) → new_foldl(yv147, yv154, yv15000, yv151, yv15000, yv152, yv153, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 3 > 5, 5 >= 6, 6 >= 7, 7 >= 8
- new_foldl5(yv206, yv207, yv208, yv209, yv210, yv211, yv212, bc) → new_foldl6(yv206, new_readInt0(yv206, yv207, yv208, bc), yv209, yv210, yv211, yv212, bc)
The graph contains the following edges 1 >= 1, 4 >= 3, 5 >= 4, 6 >= 5, 7 >= 6, 8 >= 7
- new_foldl1(yv160, yv161, yv162, yv163, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 >= 7
- new_foldl2(yv190, yv191, yv192, yv193, yv196, bb) → new_foldl4(yv190, yv191, new_pt(yv192, bb), yv193, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 4, 6 >= 5
- new_foldl0(yv190, yv191, yv192, yv193, Zero, Zero, bb) → new_foldl3(yv190, yv191, yv192, yv193, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 5
- new_foldl(yv160, yv161, yv162, yv163, Zero, Zero, yv166, ba) → new_foldl1(yv160, yv161, yv162, yv163, yv166, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 5, 8 >= 6
- new_foldl(yv160, yv161, yv162, yv163, Succ(yv1640), Zero, yv166, ba) → new_foldl0(yv160, yv161, yv162, yv163, Succ(yv162), Succ(yv166), ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 8 >= 7
- new_foldl0(yv190, yv191, yv192, yv193, Zero, Succ(yv1950), bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 6
- new_foldl3(yv190, yv191, yv192, yv193, bb) → new_foldl2(yv190, yv191, yv192, yv193, new_span2Zs1(yv193), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 6
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs0(:(yv720, yv721), yv73, ba) → new_psPs0(yv721, yv73, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs0(:(yv720, yv721), yv73, ba) → new_psPs0(yv721, yv73, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3